Inference at * 1 2 
Iof proof for Lemma absval zero:



1. i : 
2. i < 0
  ((-i) = 0)  (i = 0) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)
 b

latex

 .

Definitions

, t  T, P  Q, P  Q, P & Q, P  Q